a,b:. u,v:. gcd_p(a; b; ((u * a) + (v * b))) 

latex

Definitions	t  T, x:A. B(x), , True, T, prop{i:l}, x:A. B(x), P  Q, decidable(P), False, P  Q, A  B, A
Lemmas	decidable le, le wf, bezout ident n, true wf, squash wf, gcd p wf, gcd p neg arg